Repository navigation
wpfacts, codegen: an element site consumes its key's interval: an int32 key takes no normalizer, a non-negative one no sign test (key signs) - #14458
Merged
Conversation
added 7 commits
November 11, 2026 10:20
…key signs; WIP, not built)
…hat names an index has none)
…set fast path, so its key fact applies; wpfacts key-sign tests use two callers
…s), so the at-rest read consumes its key fact
# Conflicts: # crates/perry/src/commands/compile/compile_env/tests.rs
Pre-merge checks:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The "interval proves ≥ 0" lever (CENSUS-residual cause (i), the part N10 #14426 left: "removing it is the 'interval
proves ≥ 0' case"). An element read or store whose key is only statically numeric goes through the canonical key
split: the shared normalizer
perry_array_index_normalize_i32maps every key that is no array index (a fraction,NaN, a negative, a value past int32) to
-1, and the sign of the result picks the element tier or the exactproperty-key arm (since N10 the unsigned bound absorbs that test where a bound exists). When the whole-program facts
bound the key, none of that is needed. This PR exports the key interval of every element site and makes codegen
obey it.
Census first (main fd6e707, with the board at rest, #14439)
qb10, callgrind with
--dump-instr=yes(exact executions per instruction; anx86-64-v3build, valgrind cannot runthe native one), chess, all four workloads:
The split's own
test; js/jns/cmovnson element keys is gone already: search 0.42 M executions (the N10miss-arm exit of one evaluate read, 2 per call), evaluate 0.20 M, perft 0, legal 0: below 0.01% everywhere. The
other executed sign tests in chess code are no element keys:
make13.5 M (search) / 0.43 M (perft) / 0.40 M(legal) is the
setcall's index-clone admission ofsquareandpiece(lower_call/index_split.rs;piecereally is negative; the typed-
setlane), generatePseudo 2.0 M iscolorarithmetic, unmake 0.26 M a flag byte.What is still executed is the admission in front of that test, the normalizer call (14 instructions per
call, plus the call sequence and what the call keeps out of registers):
setclone inlined) 8.95 M,set$pshape$generic4.83 M, evaluate 3.31 M, repetitions 0.31 M, quiescence 0.26 Mown[file - 1], once per pawn)set$pshape$generic0.20 MThese are the keys codegen cannot prove an index by itself: evaluate's
own[file - 1](the pawn-file Arrays,[-1,6]), the fourthis.zobristA/B[(old + 6) * 128 + square]reads ofset(chess.ts:466-472), and inorderMoves / negamax the
VALUES[...],this.killers[ply * 2]andthis.historyScores[from * 128 + to]readsand stores (:793-797, :846-849) and the insertion sort's
result[i]/scores[j]. Statically the engine modulehas 47 normalizer calls and 44 property-key arms.
Their keys' intervals (the new probe): 36 of chess's 63 integer-key sites are non-negative int32 (
VALUES[0,8], killers[0,254], historyScores[0,16383], the pawn-file Arrays[0,7]), 9 are int32 that may benegative (the zobrist keys
[-384,1919], the board stores[-128,255],[-16,143]), 18 are integers past int32(loop counters bounded only by a
.length:[0,4294967294]for a for-of,[1,2^60]for orderMoves' insertionsort).
What changes
element_keys::collect_signs,ModuleBindings::key_signs): every element site of any operation (aread, a store, a called element) whose key is an integer Number inside the int32 range at every copy, and at every
site that shares its offset, with the hull of its interval. (
element_keys, PR-C2, covers reads only and isunchanged.) Only the key node's own Number interval counts: a key the solve resolves to the name
"3"may be thatstring at run time, so it has no key sign.
expr::index_key::{KeyFact, key_fact, store_key_fact, exact_i32}), at the three places that call thenormalizer or lower an at-rest key as a double:
index_get/runtime_key.rs). A key proven a non-negative int32 is an array index at everyevaluation: it is converted with one exact
fptosi(or is the native integer it was widened from) and entersthe element tier directly. No normalizer, no sign test, no
-1select, and the property-key arm is not emitted;the tier's own cold read serves every miss (the key may still be past the length). An int32 key that may be
negative also takes no normalizer; its sign is handled as before (N10's miss-arm exit, or the split's test), so
a negative key still reaches the runtime-key arm with its original double.
index_set.rs): an int32 key is itsi32; the guarded store's one boundidx <u capacitydeclines a negative key onto the exact helper, as it declines the normalizer's-1. A sourcestore
a[k] = vis aPutValueSetwhose index-set fast path (proxy_reflect.rs) built itsIndexSetwithelement_offset: 0; it now carries the store's site offset, so the store finds its key fact.rest_elems::lower_read): a key only the facts prove an int32 takes the int32 forms (therep-keyed tier or one
k <u floor) instead of the double round trip.Array.prototype.at(a negative index counts from the end), the$idx_u31index clones and theircall split, typed arrays (their store keeps the normalizer), at-rest stores (
rest_elems::lower_write, thetyped-
setlane's file), and a b1 call's synthesized read (it carries the body module's offset, so this module'skey facts say nothing of it).
The evaluate site (
own[file - 1], key[-1,6]; qb10,evaluate$sig, thex86-64-v3builds of rel1):Switch, probe, witness, sabotage
PERRY_FACTS_KEY_SIGN=0(off,false): wpfacts exports no key sign and codegen consumes none (= main). Acompile-cache input (
compile_env.rs, testkey_sign_switch_is_a_cache_input).PERRY_FACTS_DUMP):# key_sign module=<m> site=<offset> op=<r|w|rw> key=[lo,hi] int32=<0|1> nonneg=<0|1>,one line per element site with an integer key.
PERRY_VERIFY_FACTS=1): each consuming site first tests that its key is an integer inside int32 and,when the fact says so, not negative (
index_key::witness_sign,Fact::KeySign, "key sign"); a miss reports thefalse proof and exits 86.
key-sign-negative/PERRY_FACTS_SABOTAGE=keysign: every int32 key is claimed non-negative. Correct rc 0(the key
-2reads the named property), sabotaged rc 86, predicatekey sign.Results
Chess (qb10,
instructions:uM, one build, on vsPERRY_FACTS_KEY_SIGN=0, twice each, identical runs,checksums and PV equal in every arm).
The head's code (rel3 = d6b8328: this branch merged with main e4f004e, N12 #14442 among others):
Before merging main and before the stores consumed their key fact (rel1 = 88a78d4 on main fd6e707; the off
arm equals a separate build of that main on all four workloads):
Exact per function (callgrind,
x86-64-v3builds of rel3, off vs on; self instructions, M):perry_array_index_normalize_i32make$sigevaluate$signegamax$sig(recursive part, orderMoves inlined)set$pshape$genericNormalizer calls: search 26.84 M → 7.79 M, evaluate 1.62 M → 0, perft 0.43 M → 0, legal 0.40 M → 0. Statically the
engine module goes from 47 normalizer calls to 17 and from 44 property-key arms to 30. The callers gain more than
the 14 instructions of the call: a call site keeps its live values out of the caller-saved registers. What is left
on search (0.50%; 7.35 M of the 7.79 M calls come from orderMoves' insertion sort) are keys that are integers but
not int32 by the facts; see "Not done".
Peak RSS (
/usr/bin/time %M, KiB, 5 runs each). rel3, under load: search 25 600–26 368 on, 25 856–26 368off; perft, evaluate and legal 18 688–19 456 in both arms. rel1, quieter: search 26 880 on and off (one 26 368 in
each arm), the other three 19 456 (one or two 19 200 in either arm). On = off inside the allocator's steps.
Gates
qb10, on vs
PERRY_FACTS_KEY_SIGN=0. Gate builds: rel3 = d6b8328 (this branch merged with main e4f004e;c8adb42 adds only an edit of the new parity fixture, and its arms were rerun on rel3; the PR head then merges
main 6d3cd78, typed
set#14450 among others, with one additive conflict incompile_env/tests.rs: that head iscargo checked for perry-wpfacts, perry-codegen and perry with tests, not built or measured)and rel1 =
88a78d4 (on main fd6e707, before the stores consumed their key fact). Rows without a build name are rel3's.
PERRY_VERIFY_FACTS=1)key-sign-negative: correct rc 0, sabotaged rc 86, predicatekey sign; every older arm unchangedtest_key_sign(new),test_unsigned_bound,test_range_tightening,test_array_reps_fields,test_array_reps_loop_base_gc,test_rest_capacity,test_rest_loops,test_rest_elems,test_n1_int_temps,test_facts_int32_bindings. The at-rest forms (PERRY_REST_DIAG=1) move as they should:test_key_sign3f64→ 2rep+ 1rep_floor,test_rest_capacity5f64/ 20rep→ 3 / 22PERRY_GC_SCHEDULE_SEED=7at compile,PERRY_GC_SCHEDULE_SEED=7 PERRY_GC_SCHEDULE_RATE=1at run)test_key_sign: 107 forced copying minors, 6 208 moved objects, the same in the off arm;test_array_reps_loop_base_gc25 000 / 460 099;test_rest_capacity4 253 / 95 666. Output equals node in every armDate.now,Math.random, pids, elapsed times). Ten of them have identical IR; the eleventh,array/test_issue63_escape, has changed IR and differs only in its three printed elapsed-millisecond lines (itssum:line is equal). rel1: 2 603 programs, 104 IRDIFF, the same 11 OUTDIFF, all with identical IRPERRY_VERIFY_FACTS=1test_gap_s8b_computed_fields,test_gap_10554_fn_identity_own_module, and 12 list entries no longer in the tree). rel1: the same plustest_gap_13049_chunked_literal_birthsat the 300 s compile timeout under load# key_signlines: 554 int32, 552 of them non-negativetests/key_signs.rs, 5: a read's and a store's interval; a key that may be negative keeps its lower bound; a fraction, a string, a string that names an index, an integer past int32 and an unbounded Number have no key sign; a compound store shares its read's hull; the sabotage. codegenexpr/index_key_sign_tests.rs, 3: no fact or an interval past int32 keeps the normalizer and the property-key arm; a proven index has neither (and no miss-arm exit) in a read, a value read and a store; an int32 key that may be negative loses the normalizer and keeps its sign arm. perrykey_sign_switch_is_a_cache_inputarray_reps32, codegenrest17,proven_array19,index_get55,index_set10 passed, perrycompile_env9 passed and 1 failed (codegen_env_vars_are_build_cache_inputs, main's known failure); the new modules wpfactskey_signs(2 of 5 passed) and codegenindex_key(13 of 15 passed) had the five failures described below. Their rerun after the fix is queued on qb10 and had no cargo slot when the PR opened; the result follows as a comment-D warningsintl.rs. Not rerun on rel3scripts/check_file_size.shrustfmt --checkon every touched file: the remaining diffs are main's)A first run of the touched test modules on rel1's tree found five failures, all in this PR's new tests: three
wpfacts tests expected a hull from a single caller (the facts give the exact value), and the two codegen tests that
include a store failed because no store consumed its key fact:
a[k] = vis aPutValueSet, and its index-setfast path built the
IndexSetwithelement_offset: 0. d6b8328 carries the site offset (the at-rest store wasalready taken before that point, and no other consumer reads the offset of an
IndexSet).Not done
See FOLLOWUPS "[key-sign follow-ups]". In short:
.lengthis[0,4294967294](for-of)or the widening ladder's top (
for (let i = 1; i < xs.length; i++),j--loops). On chess that is orderMoves'insertion sort: 7.35 M of the 7.79 M normalizer calls left on search (0.50%); none on the other three workloads;
call_arg_rangescould give one);setcall's index-clone admission inmake(13.5 M sign tests on search) is the typed-setlane's.